package trabajoISW2.domain.contracts;

import java.util.List;

import tdg.contract.semanticAnnotations.Inv;
import tdg.contract.semanticAnnotations.Pos;
import tdg.contract.semanticAnnotations.Pre;
import tdg.contract.semanticAnnotations.Query;
import trabajoISW2.domain.implementations.Book;

@Inv({"getAuthorId() >= 0"})
public interface IAuthor {
	
	@Pre({"authorId >= 0 #WrongIdException", "authorId <= Integer.Max_value #WrongIdException"})
	@Pos("getAuthorId() == authorId")
	public void setAuthorId (int authorId);
	
	@Query
	public int getAuthorId ();
	
	@Pre({"name.compareTo(\"\") != 0 #WrongNameException" ,"name !=null #WrongNameException"})
	@Pos("getName().compareTo(name) == 0")
	public void setName (String name);
	
	@Query
	public String getName();
	
	@Pre({"surname.compareTo(\"\") != 0 #WrongNameException" , "surname !=null #WrongNameException"})
	@Pos("getName() == surname")
	public void setSurname (String surname);
	
	@Query
	public String getSurname ();
	
	@Pre("books !=null #IllegalArgumentException")
	@Pos("getBooks().compare(books) == 0")
	public void setBooks (List<Book> books);
	
	@Query
	public List<Book> getBooks();
	
	
	@Pre({"book !=null #IllegalArgumentException"})
	@Pos({"!getBooks().contains(book)@Pre==>getBooks().size() == getBooks().size()@Pre + 1 && getBooks().contains(book)",
		  "getBooks().contains(book)@Pre ==> getBooks().size() == getBooks().size()@Pre"})
	public void addBook (Book book);
	
	
	@Pre("book != null")
	@Pos({"!getBooks().contains(book)@Pre ==> getBooks().size() == getBooks().size()@Pre",
		   "getBooks().contains(book)@Pre ==> getBooks().size() == getBooks().size()@Pre -1 && getBooks().contains(book)"})
	public void removeBook (Book book);

	

}
